(module unifier  (lib "eopl.ss" "eopl")

  (require "drscheme-init.scm")
  (require "lang.scm")
  (require "substitutions.scm")
  (require "static-data-structures.scm")
  (require "expand-type.scm")

  ;; this provides a new view of substitutions, in which unifier
  ;; replaces extend-env as a constructor.
  (provide unifier substitution? empty-subst apply-subst)

  ;; we'll maintain the invariant that no variable bound in the
  ;; substitution occurs in any of the right-hand sides of the
  ;; substitution. 


;;;;;;;;;;;;;;;; the unifier ;;;;;;;;;;;;;;;;

;;; unifier : type * type * subst * exp -> subst OR fails


  (define unifier
    (lambda (ty1 ty2 tenv subst exp)
      
;;        (eopl:printf "entering unifier ty1 = ~s ty2 = ~s~%tenv= ~%" ty1 ty2)
;;        (eopl:pretty-print tenv)

      (let recur 

        ((ty1 (expand-type-in-tenv (apply-subst subst ty1) tenv))
         (ty2 (expand-type-in-tenv (apply-subst subst ty2) tenv))
         (subst subst))

        '(eopl:pretty-print
           (list 'entering-recur
             'ty1: ty1
             'ty2: ty2
             'subst: subst))

        (cond
          ((equal? ty1 ty2) subst)            
          ((tvar-type? ty1)
           ;; since we've already closed the type, we know that ty1 is
           ;; unbound in subst.
           (begin
             (check-no-occurrence! ty1 ty2 exp)
             (extend-subst ty1 ty2 subst)))
          ((tvar-type? ty2) (recur ty2 ty1 subst))
          ((and (proc-type? ty1) (proc-type? ty2))
           (let ((subst (recur
                          (proc-type->arg-type ty1)
                          (proc-type->arg-type ty2)
                           subst)))
             (let ((subst (recur
                            (proc-type->result-type ty1)
                            (proc-type->result-type ty2)
                            subst)))
               subst)))
          (else (raise-type-error ty1 ty2 exp))))))

  ;; is there an occurrence of tvar in ty?    If so, fail and blame
  ;; exp.  Otherwise return an unspecified value.

  (define check-no-occurrence!
    (lambda (tvar ty exp)
      (let ((ty0 ty))
        (letrec
          ((recur
             (lambda (ty)
               (cases type ty
                 (proc-type (arg-type result-type)
                   (begin
                     (recur arg-type)
                     (recur result-type)))
                 (tvar-type (serial-number)
                   (if (equal? tvar ty) 
                     (raise-occurrence-check! tvar ty0 exp)
                     #t))
                 (else #t)))))
          (recur ty)))))

  (define raise-type-error
    (lambda (t1 t2 exp)
      (eopl:error 'unifier
        "Type mismatch: ~s doesn't match ~s in ~s~%"
        (type-to-external-form t1)
        (type-to-external-form t2)
        exp)))

  (define raise-occurrence-check!
    (lambda (ty1 ty2 exp)
      (eopl:error 'check-no-occurence!
        "Can't unify: type variable ~s occurs in type ~s in expression ~s~%" 
        (type-to-external-form ty1)
        (type-to-external-form ty2)
        exp)))

  ;;  (trace unifier)

  )